(set-option :produce-unsat-model-interpolants true)
(set-logic QF_UFBV)
(declare-const bv_12-0 (_ BitVec 12))
(declare-const bv_14-0 (_ BitVec 14))
(declare-const bv_25-0 (_ BitVec 25))
(declare-const bv_16-0 (_ BitVec 16))
(declare-const bv_24-0 (_ BitVec 24))
(declare-const bv_21-0 (_ BitVec 21))
(declare-const bv_11-0 (_ BitVec 11))
(declare-const bv_18-0 (_ BitVec 18))
(declare-const bv_25-1 (_ BitVec 25))
(declare-const bv_31-0 (_ BitVec 31))
(declare-const bv_9-4 (_ BitVec 9))
(declare-const bv_20-0 (_ BitVec 20))
(declare-const bv_15-0 (_ BitVec 15))
(declare-const bv_7-9 (_ BitVec 7))
(assert (or (bvugt ((_ rotate_left 1) (concat ((_ extract 6 3) bv_16-0) ((_ repeat 8) #b01010010101))) (concat ((_ extract 6 3) bv_16-0) ((_ repeat 8) #b01010010101))) (bvult #x57 #x57) (distinct bv_14-0 bv_14-0 bv_14-0 bv_14-0)))
(check-sat-assuming-model (bv_7-9 bv_9-4 bv_11-0 bv_12-0 bv_14-0 bv_15-0 bv_16-0 bv_18-0 bv_20-0 bv_21-0 bv_24-0 bv_25-0 bv_25-1 bv_31-0 ) ((_ bv80 7) (_ bv7 9) (_ bv379 11) (_ bv1309 12) (_ bv3654 14) (_ bv21115 15) (_ bv46314 16) (_ bv204014 18) (_ bv630646 20) (_ bv91859 21) (_ bv9869541 24) (_ bv16221776 25) (_ bv8021998 25) (_ bv427384175 31) ))
(get-unsat-model-interpolant)

